Computer programs, also referred to as software programs, include codes written in a programming language to perform certain tasks in a computing device on which the computer program is executed. Examples of computing devices include, but are not limited to, a laptop, personal digital assistant (PDA), computer, mobile phone, and so on. Verification of the codes is of utmost importance for safe running of software programs. For example, it is imperative to perform defect detection in all kinds of software programs.
Static analysis is commonly used technique for sound defect detection. Static analysis includes verification by static verifiers to perform defect detection for any given input, to thereby demonstrate program correctness. Another technique for verification of software programs includes model checking. Model checking includes verifying correctness of programs by model checkers. Model checking can be utilized for effectively checking properties of programs involving scalars.
The inventors here have recognized several technical problems with such conventional systems for defect detection or verification of programs, as explained below. The verification performed by static analysis is scalable, however, it has been observed that it is imprecise for verification of codes. The technique of model checking is effective for checking properties of programs involving scalars, however, while model checking the programs involving data structures, such as arrays and C style structures, the programs often runs into a state space explosion. Since real life programs are replete with such data structures, model checking is ineffective for such programs.